FDL - Nuprl Lemma : last-transition

Nuprl Lemma : last-transition

es:ES, e:E, P:({a:E| loc(a) = loc(e)

Id}

).

e'

e.P(e') = P(e)

e'

e.(

(P(e') = P(e))) &

e''

(e',e].P(e'') = P(e)

Definitions x. t(x), A, s = t, , x(s), x.A(x), Dec(P), P Q, {T}, T, True, let x,y = A in B(x;y), Top, constant_function(f;A;B), r s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , , type List, Msg(M), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, EState(T), EOrderAxioms(E; pred?; info), IdLnk, left + right, Unit, EqDecider(T), A c B, <a, b>, first(e), P Q, ee'.P(e), P & Q, e(e1,e2].P(e), Void, e loc e' , (e <loc e'), False, t.1, ES, b, x:A B(x), ee'.P(e), {x:A| B(x)} , E, , Type, f(a), x:AB(x), x:A. B(x), Id, loc(e), x:A. B(x), t T, P Q, P Q, Atom$n, isrcv(e), (e < e')

Lemmas es-le-loc, es-isrcv-loc, es-loc wf, Id wf, bool wf, alle-le wf, es-first wf, assert wf, not wf, alle-between3 wf, es-le wf, es-locl wf, false wf, existse-le wf, true wf, squash wf, decidable equal bool, decidable not, last-event, event system wf, es-E wf